coupon.9-4.jani:model: info: coupon.9-4 is a DTMC model.
coupon.9-4.jani: info: Need 16 bytes per state.
coupon.9-4.jani: warning: The probabilities for a transition do not sum up to 1. Results will likely be affected by floating-point errors.
coupon.9-4.jani: info: Explored 21077063 states for B=5.
coupon.9-4.jani: warning: Encountered a value greater than 1 during value iteration. The final result for property "collect_all_bounded" is likely affected by floating-point errors.
Peak memory usage: 4937 MB
Analysis results for coupon.9-4.jani
Experiment B=5
+ State space exploration
State size: 16 bytes
States: 21077063
Transitions: 21077063
Branches: 24429223
Rate: 1033595 states/s
Time: 22.2 s
+ Property collect_all_bounded
Probability: 0.35851078982197176
Bounds: [0.35851078982197176, 1]
CDF: { (0, 0), ..., (2, 0), (3, 0.02862006609051592), (4, 0.16073553349925984), (5, 0.35851078982197176) }
Time: 6.1 s
+ Essential states
Iterations: 4
Essential states: 3771692
Transitions: 3771692
Branches: 7123852
Time: 3.4 s
+ Value iteration
Final error: 0
Iterations: 11
Time: 2.7 s
Exported results to file "/out.txt".